Library iso_conjugate
Require Import PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition iso_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
cTriple (q×r×v×w) (r×p×w×u) (p×q×u×v)
end.
Lemma X1_iso_conjugate_of_X2_X6 :
eq_points X_1 (iso_conjugate X_2 X_6).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition iso_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
cTriple (q×r×v×w) (r×p×w×u) (p×q×u×v)
end.
Lemma X1_iso_conjugate_of_X2_X6 :
eq_points X_1 (iso_conjugate X_2 X_6).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.